(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
D(t) → 1
D(constant) → 0
D(+(x, y)) → +(D(x), D(y))
D(*(x, y)) → +(*(y, D(x)), *(x, D(y)))
D(-(x, y)) → -(D(x), D(y))
Rewrite Strategy: FULL
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
D(+(x, y)) →+ +(D(x), D(y))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0].
The pumping substitution is [x / +(x, y)].
The result substitution is [ ].
(2) BOUNDS(n^1, INF)
(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.
(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
D(t) → 1'
D(constant) → 0'
D(+'(x, y)) → +'(D(x), D(y))
D(*'(x, y)) → +'(*'(y, D(x)), *'(x, D(y)))
D(-(x, y)) → -(D(x), D(y))
S is empty.
Rewrite Strategy: FULL
(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(6) Obligation:
TRS:
Rules:
D(t) → 1'
D(constant) → 0'
D(+'(x, y)) → +'(D(x), D(y))
D(*'(x, y)) → +'(*'(y, D(x)), *'(x, D(y)))
D(-(x, y)) → -(D(x), D(y))
Types:
D :: t:1':constant:0':+':*':- → t:1':constant:0':+':*':-
t :: t:1':constant:0':+':*':-
1' :: t:1':constant:0':+':*':-
constant :: t:1':constant:0':+':*':-
0' :: t:1':constant:0':+':*':-
+' :: t:1':constant:0':+':*':- → t:1':constant:0':+':*':- → t:1':constant:0':+':*':-
*' :: t:1':constant:0':+':*':- → t:1':constant:0':+':*':- → t:1':constant:0':+':*':-
- :: t:1':constant:0':+':*':- → t:1':constant:0':+':*':- → t:1':constant:0':+':*':-
hole_t:1':constant:0':+':*':-1_0 :: t:1':constant:0':+':*':-
gen_t:1':constant:0':+':*':-2_0 :: Nat → t:1':constant:0':+':*':-
(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
D
(8) Obligation:
TRS:
Rules:
D(
t) →
1'D(
constant) →
0'D(
+'(
x,
y)) →
+'(
D(
x),
D(
y))
D(
*'(
x,
y)) →
+'(
*'(
y,
D(
x)),
*'(
x,
D(
y)))
D(
-(
x,
y)) →
-(
D(
x),
D(
y))
Types:
D :: t:1':constant:0':+':*':- → t:1':constant:0':+':*':-
t :: t:1':constant:0':+':*':-
1' :: t:1':constant:0':+':*':-
constant :: t:1':constant:0':+':*':-
0' :: t:1':constant:0':+':*':-
+' :: t:1':constant:0':+':*':- → t:1':constant:0':+':*':- → t:1':constant:0':+':*':-
*' :: t:1':constant:0':+':*':- → t:1':constant:0':+':*':- → t:1':constant:0':+':*':-
- :: t:1':constant:0':+':*':- → t:1':constant:0':+':*':- → t:1':constant:0':+':*':-
hole_t:1':constant:0':+':*':-1_0 :: t:1':constant:0':+':*':-
gen_t:1':constant:0':+':*':-2_0 :: Nat → t:1':constant:0':+':*':-
Generator Equations:
gen_t:1':constant:0':+':*':-2_0(0) ⇔ t
gen_t:1':constant:0':+':*':-2_0(+(x, 1)) ⇔ +'(t, gen_t:1':constant:0':+':*':-2_0(x))
The following defined symbols remain to be analysed:
D
(9) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
D(
gen_t:1':constant:0':+':*':-2_0(
n4_0)) →
*3_0, rt ∈ Ω(n4
0)
Induction Base:
D(gen_t:1':constant:0':+':*':-2_0(0))
Induction Step:
D(gen_t:1':constant:0':+':*':-2_0(+(n4_0, 1))) →RΩ(1)
+'(D(t), D(gen_t:1':constant:0':+':*':-2_0(n4_0))) →RΩ(1)
+'(1', D(gen_t:1':constant:0':+':*':-2_0(n4_0))) →IH
+'(1', *3_0)
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(10) Complex Obligation (BEST)
(11) Obligation:
TRS:
Rules:
D(
t) →
1'D(
constant) →
0'D(
+'(
x,
y)) →
+'(
D(
x),
D(
y))
D(
*'(
x,
y)) →
+'(
*'(
y,
D(
x)),
*'(
x,
D(
y)))
D(
-(
x,
y)) →
-(
D(
x),
D(
y))
Types:
D :: t:1':constant:0':+':*':- → t:1':constant:0':+':*':-
t :: t:1':constant:0':+':*':-
1' :: t:1':constant:0':+':*':-
constant :: t:1':constant:0':+':*':-
0' :: t:1':constant:0':+':*':-
+' :: t:1':constant:0':+':*':- → t:1':constant:0':+':*':- → t:1':constant:0':+':*':-
*' :: t:1':constant:0':+':*':- → t:1':constant:0':+':*':- → t:1':constant:0':+':*':-
- :: t:1':constant:0':+':*':- → t:1':constant:0':+':*':- → t:1':constant:0':+':*':-
hole_t:1':constant:0':+':*':-1_0 :: t:1':constant:0':+':*':-
gen_t:1':constant:0':+':*':-2_0 :: Nat → t:1':constant:0':+':*':-
Lemmas:
D(gen_t:1':constant:0':+':*':-2_0(n4_0)) → *3_0, rt ∈ Ω(n40)
Generator Equations:
gen_t:1':constant:0':+':*':-2_0(0) ⇔ t
gen_t:1':constant:0':+':*':-2_0(+(x, 1)) ⇔ +'(t, gen_t:1':constant:0':+':*':-2_0(x))
No more defined symbols left to analyse.
(12) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
D(gen_t:1':constant:0':+':*':-2_0(n4_0)) → *3_0, rt ∈ Ω(n40)
(13) BOUNDS(n^1, INF)
(14) Obligation:
TRS:
Rules:
D(
t) →
1'D(
constant) →
0'D(
+'(
x,
y)) →
+'(
D(
x),
D(
y))
D(
*'(
x,
y)) →
+'(
*'(
y,
D(
x)),
*'(
x,
D(
y)))
D(
-(
x,
y)) →
-(
D(
x),
D(
y))
Types:
D :: t:1':constant:0':+':*':- → t:1':constant:0':+':*':-
t :: t:1':constant:0':+':*':-
1' :: t:1':constant:0':+':*':-
constant :: t:1':constant:0':+':*':-
0' :: t:1':constant:0':+':*':-
+' :: t:1':constant:0':+':*':- → t:1':constant:0':+':*':- → t:1':constant:0':+':*':-
*' :: t:1':constant:0':+':*':- → t:1':constant:0':+':*':- → t:1':constant:0':+':*':-
- :: t:1':constant:0':+':*':- → t:1':constant:0':+':*':- → t:1':constant:0':+':*':-
hole_t:1':constant:0':+':*':-1_0 :: t:1':constant:0':+':*':-
gen_t:1':constant:0':+':*':-2_0 :: Nat → t:1':constant:0':+':*':-
Lemmas:
D(gen_t:1':constant:0':+':*':-2_0(n4_0)) → *3_0, rt ∈ Ω(n40)
Generator Equations:
gen_t:1':constant:0':+':*':-2_0(0) ⇔ t
gen_t:1':constant:0':+':*':-2_0(+(x, 1)) ⇔ +'(t, gen_t:1':constant:0':+':*':-2_0(x))
No more defined symbols left to analyse.
(15) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
D(gen_t:1':constant:0':+':*':-2_0(n4_0)) → *3_0, rt ∈ Ω(n40)
(16) BOUNDS(n^1, INF)